Add knowledge about floor/ceil bounds #718
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
In the RIA prelude, we have axioms with semantic triggers to propagate bounds on reals to bounds on integers using
real_of_int
(real_of_int_to_int_1
andreal_of_int_to_int_2
).These state respectively that:
If
real_of_int(i) ≤ y
holds in the reals, theni ≤ int_floor(y)
holds in the integers.If
y ≤ real_of_int(i)
holds in the reals, thenint_ceil(y) ≤ i
holds in the integers.This patch adds the corresponding propagations from bounds on integers to bounds on reals. More precisely it adds the propagations:
If
int_floor(x) ≤ i
holds in the integers,x < real_of_int(i + 1)
holds in the realsIf
i ≤ int_floor(x)
holds in the integers,real_of_int(i) ≤ x
holds in the realsIf
int_ceil(x) ≤ i
holds in the integers,x ≤ real_of_int(i)
holds in the realsIf
i ≤ int_ceil(x)
holds in the integers,real_of_int(i - 1) < x
holds in the reals(Note that the test has "unknown" expected but it should be SAT -- this is because the ria prelude is disabled currently)